Model-based design (MBD) is increasingly being used to develop embedded control systems for automotive applications. MBD provides a framework under which system design specifications and performance models may be created and automatic code generation, calibration, and integrated testing may be performed. Proper tools for performing MBD activities may be required to ensure an efficient, effective development process that satisfies software quality and operational standards. Techniques for evaluating embedded controller designs developed during the MBD process may include simulation, hardware in-the-loop (HIL) testing, and calibration. Improving the efficiency and effectiveness of these testing activities is important, since they account for a significant portion of the system design and deployment cost. Additionally, the tests directly affect product performance measures, such as quality, and efficiency. Despite this, methods for performing these tests are often ad hoc and usually lack formal specifications against which an engineer may test.
Difficulties contributing to the deficiencies in testing procedures are a consequence of the natural intractability of the verification task for real-time control systems. While techniques such as model checking have successfully been applied to computer hardware to verify correct operation, verification of real-time control systems (e.g., for automotive applications) has been shown to be undecideable; that is, is has been proven that no computer algorithm can solve the general problem of verifying correct operation of a real-time computer control system.
Techniques, however, do exist for proving properties of real-time control systems for specific cases. Lyapunov techniques can prove certain correctness properties for dynamical systems. Such Lyapunov notions can be applied to real-time control systems, but they are only tractable for special classes of systems and can only be applied at the earliest stages of the MBD process (e.g., the initial design or specification stage). Accordingly, it may be advantageous to be able to apply such techniques to the later stages of the MBD process. This type of analysis would increase confidence in the correctness of the design and increase the efficiency of the testing process, thereby reducing cost, and decreasing the possibility of errors in the control design (resulting in a decreased chance of quality problems and safety issues).